es:ES, l1, l2:IdLnk, tg1, tg2:Id.
es-responsive(es;l1;tg1;l2;tg2)
 (f:{e:E| kind(e) = rcv(l1,tg1)  Knd} {e:E| kind(e) = rcv(l2,tg2)  Knd} 
 (Bij({e:E| kind(e) = rcv(l1,tg1)  Knd} ;{e:E| kind(e) = rcv(l2,tg2)  Knd} ;f)) 

latex

Definitions

x:A. B(x), P  Q, t  T, P & Q, x:A. B(x), A c B, , , t.1, x. t(x), Bij(A;B;f), Inj(A;B;f), Surj(A;B;f), T, True, A, es-responsive(es;l1;tg1;l2;tg2), e=rcv(l,tg). P(e), e=rcv(l,tg). P(e), {T}, x(s), P  Q, P  Q, SqStable(P), (e <loc e'), False, Dec(P)

Lemmas

es-responsive wf, Id wf, IdLnk wf, event system wf, Knd wf, es-kind wf, rcv wf, es-E wf, es-le wf, es-sender wf, es-kind-rcv, es-locl wf, pi1 wf, biject wf, es-axioms, es-le-loc, lsrc wf, squash wf, true wf, ldst wf, es-loc-rcv, sq stable from decidable, assert wf, es-isrcv wf, decidable assert, es-le-not-locl, es-loc-pred, es-locl-iff, decidable equal Kind, es-locl transitivity2, es-locl irreflexivity, es-locl transitivity1